这节用三个例子学习UPPAAL的使用。

UPPAAL里支持用CTL公式描述功能安全性质： A [ ]   φ A ⟨ ⟩   φ E [ ]   φ E ⟨ ⟩   φ \begin{aligned} & A[] \ \varphi \\ & A\langle \rangle \ \varphi \\ & E[] \ \varphi \\ & E\langle \rangle \ \varphi \end{aligned} ​A[] φA⟨⟩ φE[] φE⟨⟩ φ​

其中 A A A表示 A l l All All（所有路径）， E E E表示 E x i s t Exist Exist（存在某个路径）， [ ] [] []表示 G l o b a l l y Globally Globally（路径上的所有状态）， ⟨ ⟩ \langle \rangle ⟨⟩表示 F u t u r e Future Future（未来某个状态）。

选项卡分为编辑器、模拟器、验证器。

编辑器用于在一个项目里进行建模，每个项目有一个全局声明，可以用来声明全局变量（所有模板及其实例都可见），可以添加若干Template（就是进程模板），以及在模型声明中对进程模板进行例化，对整个系统的组织进行描述。

在这里建立好模型后，点击【工具->检查语法】，如果无误的话右下方的框里就没有东西。

模拟器里可以看到所建立的所有模型及其例化后的TS，可以选择转换进行单步模拟执行，模拟器也用于性质验证不通过时候给出反例，可以从上到下把整个Trace重放一遍，每个实例状态机上当前所处的状态会标红。 验证器里可以书写性质并验证，获得验证结果。在【待验证性质】处书写CTL公式，在【备注】处可以对这个公式进行描述，因为有些公式很难直观看出要表达什么，这个也会保存下来，添加到性质列表里之后就能验证了，然后结果会显示在下面的框里。

在Template里建一个最简单的TS模型： UPPAAL里可以设置状态为初始状态，但是不需要指定终止状态，这个是自动判断的。

接下来可以看下模型声明的部分，还是使用默认的，就是把这个模型例化得到Process，然后整个系统就是这个例化对象的执行：

到模拟器里可以看到这个模型：

选中这个例化对象Process，点击【下一步】就能让它往下走： 这个TS走到end状态就无路可走了，所以【使能迁移】里也没有选项了。

到验证器里，先验证一个E Process.end，这表示存在一个路径，未来能让实例Process到达end这个状态，验证结果通过，这是显而易见的。

再验证一个A Process.end，这表示对所有的路径，都能未来让实例Process到达end这个状态，验证结果不通过：

这是因为一个TS的Guard条件通过了，只是表示“这条迁移可以发生”，但不代表一定会发生，在这个模型里，完全可以一直停留在start状态，而不发生这条唯一的迁移，所以这个性质是不满足的。

要让迁移在一定条件下一定发生，可以给状态设置不变性，一旦不变性不满足了，就无法停留在这个状态了，也就强迫它进行迁移，到其它状态去。

这个互斥通信里涉及两个进程，但是它们的行为可以用一个模板来描述，先给这个模板建模（双击转移边就能设置边上的条件和动作，这里只用到卫条件Guard和变量更新Update）：

其中有四个状态，idle、want、wait、CS，分别表示闲置状态、想进入（临界区）、等待、临界区。req_self表示自己是否请求进入临界区，turn表示现在轮到谁，req_other表示对方是否请求进入临界区。可以看出它们都是双方要知道的信息，turn就是一个全局信息，而req_self和req_other对双方而言是反过来的。me表示自己的ID，对双方而言一个取1一个取2，这是进程自己的局部变量，两方分别持有。

这个状态机的行为大意就是，一开始给自己req_self设置为1表示想要进入临界区了，然后礼貌地将turn设置为对方的ID，想让对方先走，然后检查如果turn是me（轮到自己，即对方让自己先走），或者req_other是0（对方压根没有进临界区的想法），这时候自己就可以进入临界区，进完之后将req_self设置回0，回到最开始的闲置状态。

在图的上方设置这个进程模板的名字是mutex，然后设置了它的参数表：

可以简单的把参数表理解成进程模板例化时候的构造器，这里有三个参数：

接下来书写模型声明的部分，即为这个进程模板mutex例化为P1和P2，全局变量req1和req2保存两方有没有请求进入临界区（用传引用的方式传进去），整个系统就是这两个例化的进程：

然后在声明部分声明一下前面提到的三个全局变量：

检查语法无误，就可以去模拟器里单步模拟执行，还能看到全局变量实时的值：

接下来验证性质，一个是A[] not(P1.CS and P2.CS)，表示对所有的路径的所有状态，都不会有两者不会同时处在临界区的情况，验证可以通过；另一个是E P1.CS，表示存在一个路径，在未来某个状态例化进程P1处在CS状态，即P1有机会进入临界区，验证也是通过的。

这个模型是正确的，为了演示反例，先给它故意改成错误的，这里把模板里的req_other==0改成req_other==1。改了模板之后，为了验证之后得到反例，要去点一下【模拟器】然后重新加载一下模型。

为了能在验证后得到反例，这里要在菜单栏勾上【菜单->诊断路径->某些】。

进入验证器里，重新验证第一条（不会同时进入临界区）性质，验证不通过，这时候进入模拟器，可以看到给出了反例：

点击【重放】就能像放动画一样让它从头到尾跑一遍了。

这个例子里需要在一个项目里使用两个进程模板，添加的方式是【编辑->添加模板】。

模板P1就是一个自循环，Guard条件x>=2时进行Sync（同步通信），往通道reset上发送重置信号（!表示发送，?表示接收，和学CSP时候一样）：

模板Obs（意为Observer，观察者），行为就是接收到通道reset上的信号之后，就将全局变量x设置为0（其实是表示时钟重置，要从后面声明的地方看出这一点）： 这里要注意taken上有个C，因为它勾选了Commited，关于这个选项的官方解释如下：

Like urgent locations, committed locations freeze time. Furthermore, if any process is in a committed location, the next transition must involve an edge from one of the committed locations. Committed locations are useful for creating atomic sequences and for encoding synchronization between more than two components. Notice that if several processes are in a committed location at the same time, then they will interleave.

大意就是被标记Commited的状态会冻结时间流逝，而且下一次转移一定从某个Commited状态开始（要把所有冻结时间的状态走出去，才能考虑普通的状态），如果多个状态被标Commited，它们就按Interleaving算。

书写模型声明部分，这里可以不去显式做例化，直接两个模板拿来用：

设置全局变量，x是时钟（clock），reset是通道（chan）：

语法检查通过就可以去模拟，就是P1发信号然后Obs重置然后再回来：

可以看到，因为taken状态被标Commited，所以到这里必须把这个Obs走出这个状态才能往下走，即图中圈起来部分——总是先让Obs回到idle状态。

验证A[] Obs.taken imply x>=2，即对所有路径的所有状态都有，如果Obs到达了taken状态，一定有时钟x满足x>=2，验证是通过的，因为x>=2才能发信号到reset通道上，让Obs同步接收之后进到taken状态。

验证E Obs.idle and x>3，即存在某个路径上某个状态，Obs在idle状态闲置时就有x>3了，验证也是通过的。这条性质直观上可能让人感觉不能通过（因为x>=2是P1迁移的条件），但是回想最开始学的，这些Guard条件满足时只表示“迁移可以发生”，而不是一定会发生，所以P1完全可以x超过3了还不发生迁移，也就不会往reset发信号，所以Obs也就处在最开始的idle状态了。

上面4.3节的第二条性质验证通过，是因为总是能一直停留在某个状态，如何解决这个问题，就是可以去给状态添加一个有关时钟的不变性条件，当时间流逝使得这个条件不满足时候，就不得不离开这个状态往下走了，这也符合平时对某些实时系统的建模需求。

双击状态在【Invariant】里写就行了，这里是为P1的loop状态添加了x=2 and x2，即可能Obs在idle状态时，时钟x是大于2的，验证通过。因为这个也是满足loop里x不超过3的不变性的，完全可以等到2.999...。

但是它对性质E Obs.idle and x>3就是不满足的了，因为一旦x>3，P1就必须从loop迁移走，发出的信号让Obs也同步离开idle。

为了加深对不变性的理解，这里尝试将不变性移除，而改到迁移的Guard条件里：

这个新的模型对性质A[] Obs.taken imply (x>=2 and x2仍然是验证通过的，但是语义显然和刚才不一样了，可以体现在对性质E Obs.idle and x>3，它又可以验证通过了（因为现在又没有了对loop停留的限制）：